Nuprl Lemma : atom-free-dep-function
0,22
postcript
pdf
A
:Type,
B
:(
A
Type). AtomFree(Type;
A
)
AtomFree(
A
Type;
B
)
AtomFree(Type;
x
:
A
B
(
x
))
latex
Definitions
Type
,
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
AtomFree(
T
;
x
)
,
f
(
a
)
,
x
(
s
)
,
x
.
A
(
x
)
,
P
Q
Lemmas
atom-free
wf
origin
A:Type, B:(A
Type). AtomFree(Type;A) 
AtomFree(AType;B) AtomFree(Type;x:AB(x)) A:Type, B:(AType). AtomFree(Type;A) AtomFree(AType;B) AtomFree(Type;x:AB(x)) 
TB(x)x:A. B(x)
x.A(x) Q